occurs check

単一化の際に型の出現検査をする

一つの型変数 = なんかの型を考えたときに、「左辺の型変数」が右辺に含まれていないかどうか、を判定する

含まれている場合、どうごにょっても無理になるので、型に不整合があると判断し、処理を中断する

無理な例

CVar 1 == (CInt -> (CVar 1 -> CBool))

一つの型変数 == なんかの型という等式を考えている

CVar 1は型変数

この等式を満たすような型CVar 1は存在しない

なぜなら絶対に右辺のほうが大きな型になるから

「左辺の型変数」が右辺に含まれていない、というのが条件になる

右辺が型変数を含まない型の場合も問答無用で結果はFalseになる

関数の例

上の例に合わせるなら左辺 -> 右辺 -> 結果

code:hs

occur :: Int -> Type -> TI Bool

返り値はbool

第一引数が、IntになっているのはTVarのidをIntにしているから

TVar ここ

参考